Propositions as Types
Propositions as Types(型としての命題)
数理論理学での論理は、依存型理論での型と本質的に同じと見なすことができるというやつ
命題(proposision) = 型(type)
$ \mathrm{ proof : Proposition} \cong \mathrm{term : Type}
証明を関数(λ項: 証明項と呼ぶ)、命題を証明項のデータ型とみなす
$ \begin{array}{c|c} \mathrm{英語} & \mathrm{型理論} \\ \hline \mathrm{True} & \mathbf{1} \\ \mathrm{False} & \mathbf{0} \\ \text{A and B} & A \times B \\ \text{A or B} & A + B \\ \text{If A then B} & A \rightarrow B \\ \text{A if and only if B} & (A \rightarrow B ) \times (B \rightarrow A) \\ \text{Not A} & A \rightarrow \mathbf{0} \end{array}
$ \begin{array}{c|c} \mathrm{論理} & \mathrm{型理論} \\ \hline \mathrm{True} & \mathbf{1} \\ \mathrm{False} & \mathbf{0} \\ A \land B & A \times B \\ A \lor B & A + B \\ A \implies B & A \rightarrow B \\ A \iff B & (A \rightarrow B ) \times (B \rightarrow A) \\ \lnot A & A \rightarrow \mathbf{0} \end{array}
$ \mathbf{0} は空型(empty type)
and(A∧B)、$ \times (デカルト積) 証明Aと証明B
$ \frac{x: A \quad y: B }{(x, y) : A \times B}
or(P∨Q)、非交和
$ A + B
If A and Bは関数f : A → Bに対応
A, Bは型
否定(negation)の$ \lnot A は$ A \to \mathbf{0} に対応
関連
参考
メモ
https://youtu.be/q7zmw8DKx14?si=b433QNewETrOS5Eo